b:, T:Type, A, B:T List, x:T. (x  if b A else B fi)  b & (x  A)  b & (x  B) 

latex

Definitions	Unit, b, , Prop, x:A. B(x), P  Q, P  Q, True, t  T, P  Q, (x  l), {T}, P & Q, A, P  Q, False
Lemmas	false wf, not wf, l member wf, true wf, bool wf